Formal Verification and Auditing of Smart Contracts

1. Introduction to Smart Contracts

Use Cases

2. Importance of Security in Smart Contracts

Need for Formal Verification

To enhance the security of smart contracts, formal verification techniques are essential to ensure that contracts behave as intended under all circumstances.

3. What is Formal Verification?

Definition

Comparison with Traditional Testing

Benefits

4. Understanding Formal Models

What is a Formal Model?

Types of Formal Models

  1. High-Level Models:

    • Focus on the overall behavior of the smart contract.
    • Use finite state machines (FSM) to represent state transitions.
    • Example: Modeling a voting contract as an FSM with states for “Voting Open,” “Voting Closed,” and “Results Announced.”

  2. Low-Level Models:

    • Provide detailed analysis of the contract’s execution.
    • Use control flow graphs (CFG) and program traces.
    • Example: Analyzing how each function call changes the state of a smart contract, identifying potential vulnerabilities.

Benefits of Formal Models

5. What is a Formal Specification?

Definition

Importance

Example of Formal Specification

Formal Specification
1. Language-Level Specification
2. Bytecode-Level Specification
High-level Business Logic of the Contract
Derived from Informal Specifications like Whitepapers
Ensures Code Meets Functional Requirements
Behavior of the Compiled Contract in a Virtual Machine
Ensures Compiled Bytecode Matches High-Level Logic

6. Types of Formal Specifications

1. High-Level Specifications

Example of Safety Property

2. Low-Level Specifications

Hoare Triple Example

7. Techniques for Formal Verification

1. Model Checking

Pros and Cons

2. Theorem Proving

Pros and Cons

3. Symbolic Execution

Benefits

8. Using Formal Verification Tools

  1. K Framework:

    • A framework for defining programming languages and verifying their properties.
    • Allows for executable specifications and formal analysis of smart contracts.

  2. Dafny:

    • A programming language designed for verifying functional correctness.
    • Includes built-in support for assertions and contracts, making it easy to specify properties.

Case Studies

Slide 9: Summary Pros and Cons of Formal Verification

Formal verification is a mathematical approach used to prove or disprove the correctness of a system with respect to a certain formal specification or property. It has several advantages and challenges, especially in the context of software development, particularly in critical areas such as smart contracts, aerospace, healthcare systems, and other high-assurance fields.

Pros of Formal Verification

  1. Mathematical Certainty:

    • Benefit: Formal verification provides mathematical guarantees that a system adheres strictly to its specifications. Unlike traditional testing, which can only cover a finite number of cases, formal verification checks all possible inputs and states.
    • Use Case: In systems where safety, security, and correctness are paramount (e.g., cryptography, aerospace, medical devices), this mathematical rigor ensures that no critical flaws remain undetected.

  2. Detection of Edge Cases:

    • Benefit: Traditional testing may miss certain edge cases, particularly those that are rare or difficult to simulate. Formal verification analyzes all potential cases, including corner cases, to ensure the system behaves as expected under all possible conditions.
    • Use Case: In decentralized finance (DeFi), smart contracts handling large sums of money or sensitive operations can be vulnerable to rare but catastrophic bugs. Formal verification ensures that no obscure scenario could lead to a security breach.

  3. Improved Security and Reliability:

    • Benefit: In systems where security is critical, formal verification can ensure that the system is free from vulnerabilities like buffer overflows, underflows, or logical inconsistencies.
    • Use Case: Industries such as defense, finance, and blockchain applications benefit significantly from this approach, where security flaws can have severe consequences.

  4. Prevention of Costly Errors:

    • Benefit: Bugs in critical systems can lead to substantial financial loss, data breaches, or even life-threatening situations. Formal verification can prevent these by identifying errors early in the development process, thereby reducing the need for costly patches or fixes later on.
    • Use Case: Airbus uses formal methods to ensure the safety and reliability of its aircraft control systems, reducing the chance of fatal failures.

  5. Increased Trustworthiness and Compliance:

    • Benefit: Formal verification can be used to meet regulatory standards and provide higher assurance of safety and correctness. This is crucial in regulated industries where software failure can lead to non-compliance with laws and standards.
    • Use Case: Medical software for life-support systems must meet stringent regulatory requirements, and formal verification can help ensure compliance with these.

  6. Proof of Compliance with Complex Properties:

    • Benefit: Some properties, such as privacy, fairness, or non-repudiation in digital systems, can be challenging to validate using traditional methods. Formal verification allows developers to prove that the system respects these complex properties.
    • Use Case: Cryptographic systems, where proving zero-knowledge properties or other advanced cryptographic guarantees is crucial, benefit from formal verification.

Cons of Formal Verification

  1. Complexity and Scalability:

    • Challenge: Formal verification can be extremely complex and resource-intensive, especially for large systems with millions of lines of code. It may require abstracting or simplifying certain parts of the system to make verification feasible.
    • Limitation: Large-scale systems (like operating systems or large enterprise software) may be difficult to verify completely due to the high computational requirements and time involved.

  2. High Cost and Time-Consuming:

    • Challenge: Developing formal specifications and carrying out formal verification can be more time-consuming and expensive than traditional testing. It requires specialized knowledge, tools, and a thorough understanding of formal logic and mathematics.
    • Limitation: Many businesses cannot afford to employ formal verification throughout their entire software lifecycle, as it may slow down time-to-market and increase development costs.

  3. Limited Availability of Expertise:

    • Challenge: Formal verification requires a highly specialized skill set that not all developers or engineers possess. This creates a barrier to entry, as finding experts in this field can be challenging and costly.
    • Limitation: Smaller companies or startups may find it difficult to integrate formal methods into their development process due to the scarcity of experts and the need for specialized tools.

  4. Abstraction and Oversimplification:

    • Challenge: In some cases, the formal models used to verify a system may be oversimplified to make verification feasible. This could lead to situations where the formal model does not accurately represent the real system.
    • Limitation: Systems with heavy reliance on external dependencies or real-time environments may require abstractions that miss critical real-world issues.

  5. Not a Guarantee of Overall Correctness:

    • Challenge: Formal verification can only prove the correctness of a system with respect to the specifications provided. If the specification itself is flawed or incomplete, formal verification will not catch these issues.
    • Limitation: The entire verification process depends on the quality of the specification. Poorly defined specifications can lead to incorrect conclusions about the system’s behavior.

  6. Limited Tool Support:

    • Challenge: While tools for formal verification exist (e.g., Coq, Isabelle, TLA+, and Z3), they can be difficult to use and may not integrate seamlessly with modern development environments. Moreover, different tools are better suited for specific kinds of verification, making the choice of tools critical.
    • Limitation: Developers often face challenges integrating formal verification tools into their existing workflows, which may discourage its adoption.

  7. Applicability to Specific Domains:

    • Challenge: Not all software systems require formal verification. For many low-risk, less critical applications, the benefits may not justify the time and expense. In these cases, traditional testing approaches might be sufficient.
    • Limitation: In areas like web or mobile app development, where the consequences of failure are not catastrophic, the overhead of formal verification may outweigh the potential gains.

Slide 10: Formal Verification vs Other Methods

Slide 11: Introduction to K Framework

Slide 12: K Framework Components

Slide 13: KEVM (K-Ethereum Virtual Machine)

Slide 14: Solidity Smart Contract Example

Slide 15: High-Level Specification in K

Slide 16: Bytecode-Level Specification Example

Slide 17: Conducting Smart Contract Audits

Slide 18: Writing Comprehensive Audit Reports

Slide 19: Third-Party Auditing Services

Slide 20: Case Study: Formal Verification

Let’s walk through a practical example of how formal verification can be applied to an ICO smart contract. We will use a simplified Solidity contract, and then proceed through the steps of defining the formal specification, running verification with KEVM, and detecting a potential error in the contract.

Smart Contract Code Example: Simple ICO in Solidity

Here’s a basic ICO smart contract in Solidity:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;

contract SimpleICO {
    address public owner;
    uint256 public hardCap;
    uint256 public amountRaised;
    mapping(address => uint256) public balances;

    constructor(uint256 _hardCap) {
        owner = msg.sender;
        hardCap = _hardCap;
        amountRaised = 0;
    }

    modifier onlyOwner() {
        require(msg.sender == owner, "Not authorized");
        _;
    }

    function contribute() public payable {
        require(msg.value > 0, "Contribution must be greater than 0");
        require(amountRaised + msg.value <= hardCap, "Hard cap reached");

        balances[msg.sender] += msg.value;
        amountRaised += msg.value;
    }

    function withdrawFunds() public onlyOwner {
        require(amountRaised >= hardCap, "Hard cap not reached");
        payable(owner).transfer(amountRaised);
    }

    function refund() public {
        require(amountRaised < hardCap, "Refunds not allowed after hard cap");
        uint256 contributed = balances[msg.sender];
        require(contributed > 0, "No contributions to refund");

        balances[msg.sender] = 0;
        payable(msg.sender).transfer(contributed);
    }
}

Steps in Formal Verification

1. Define the Specification: High-Level and Bytecode

The formal specification consists of both high-level functional requirements and low-level bytecode properties.

High-Level Specification:

The key functional requirements for this ICO contract are:

Example Requirements:
Bytecode-Level Specification:

At the bytecode level, we ensure that:

2. Use KEVM to Run Verification

Using the K Framework and KEVM, we can formally verify that the contract adheres to its specification. Here’s the process:

  1. Translate the Contract to KEVM: Convert the compiled bytecode of the Solidity contract into KEVM’s formal model.
  2. Apply Specifications: Encode the formal specification into KEVM. This will include the functional requirements (e.g., no overflow, correct access control) and low-level bytecode checks.
  3. Run the Verification: Execute the KEVM engine to check whether the contract satisfies the formal specifications.

For example, the following properties could be encoded:

3. Error Handling: Detecting Bugs Like Overflow

Now, let’s simulate a bug in the code and see how formal verification would catch it.

Example Error: Changing require(_hardCap >= amountRaised) to require(_hardCap <= amountRaised) in withdrawFunds()

Imagine we accidentally modify the condition in the withdrawFunds() function, introducing a subtle bug:

function withdrawFunds() public onlyOwner {
    // Bug: incorrect condition
    require(amountRaised <= hardCap, "Hard cap not reached");
    payable(owner).transfer(amountRaised);
}

This error allows the owner to withdraw funds before the hard cap is reached, violating the original contract logic.

KEVM Verification Process:

When we run the formal verification with this bug in place, KEVM detects that the property of the withdrawFunds function (which requires the hard cap to be reached before withdrawing) is violated. The bytecode no longer conforms to the formal specification because the condition require(amountRaised >= hardCap) is incorrectly modified.

Other Possible Bugs Detected:

Conclusion: Benefits of Formal Verification in Smart Contracts

By applying formal verification to this simple ICO contract, we ensure that:

Slide 21: Conclusion